/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking.role;

import caetus.modelChecking.goal.ModelGoalMap;
import caetus.modelChecking.variable.ModelConstants;
import caetus.modelChecking.variable.ModelVariable;
import caetus.pkcs11.tokenCapabilities.TokenCapabilities;
import java.util.Collections;
import java.util.LinkedList;
import java.util.List;

/**
 *
 * @author Josef Hertl
 */
public class ModelEnvironment extends ModelRole {

    private ModelSession session;

    /**
     * Does not require name, since that always is "environment".
     *
     * @param modelSession The session created by this environment
     * @param capabilities The passed capabilities of the token.
     */
    public ModelEnvironment(ModelSession modelSession, TokenCapabilities capabilities) {
        super("environment", capabilities);
        this.session = modelSession;
    }

    @Override
    public String makeRole() {
        String result = makeRoleStart();
        result += "def=\n";
        List<ModelVariable> variables = new LinkedList<ModelVariable>(session.getGlobalVariables());
        Collections.sort(variables);
        List<ModelVariable> constants = new LinkedList<ModelVariable>(variables);
        constants.addAll(ModelGoalMap.getProtocolIDs());
        constants.addAll(ModelConstants.getAllTextConstants());
        result += prepareConstants(constants);
        result += makeIntruderKnowledge(constants);
        result += makeComposition(variables);
        result += makeRoleEnd();
        return result;
    }
    
    /**
     * Prepares intruder knowledge. It includes everything except the data that are secret and symmetric keys
     * @return hlpsl-ready specification of intruder knowledge.
     */
    private String makeIntruderKnowledge(List<ModelVariable> constants) {
        String result = "\n\nintruder_knowledge = {";
        List<ModelVariable> intruderKnowledge = new LinkedList<ModelVariable>();
        for (ModelVariable modelVariable : constants) {
            if (!modelVariable.getVariableType().contains("symmetric")) {
                intruderKnowledge.add(modelVariable);
            }
        }
        intruderKnowledge.removeAll(ModelGoalMap.getProtocolIDs());
        intruderKnowledge.removeAll(ModelGoalMap.getAllSecretVariables());
        
        for (int i = 0; i < intruderKnowledge.size(); i++) {
            if (i!=0) {
                result += ",";
            }
            result += intruderKnowledge.get(i).getVariableName().toLowerCase();
        }
        result += "}\n";
        return result;
    }

    /**
     * @return hlpsl-ready representation of the composition
     */
    private String makeComposition(List<ModelVariable> variables) {
        String result = "\n\ncomposition\n";
        List<ModelVariable> persons = new LinkedList<ModelVariable>();
        for (ModelVariable modelVariable : variables) {
            if (modelVariable.getVariableType().contains("agent") && !modelVariable.getVariableName().contains("T")) { //T in the name is used to signal a token
                persons.add(modelVariable);
            }
        }
        result += makeCompositionRowReplaceWithIntruder(variables, null);
        for (int i = 0; i < persons.size(); i++) {
            result += makeCompositionRowReplaceWithIntruder(variables, persons.get(i));
        }

        return result;
    }

    /**
     * Makes a row in the composition.
     *
     * @param variable The agent that will be replaced by the intruder (= will
     * play the intruder role).
     * @return hlpsl-ready row in the composition.
     */
    private String makeCompositionRowReplaceWithIntruder(List<ModelVariable> variables, ModelVariable variable) {
        if (variable != null && !variable.getVariableType().contains("agent")) {
            throw new IllegalArgumentException("The type of replaced variable must be an agent!");
        }
        String result = "";
        if (variable == null) {
            result += "     ";
        } else {
            result += "  /\\ ";
        }
        result += "session(";
        for (int i = 0; i < variables.size(); i++) {
            if (i != 0) {
                result += ",";
            }
            if (variables.get(i).equals(variable)) {
                result += "i";
            } else {
                result += variables.get(i).getVariableName().toLowerCase();
            }
        }
        result += ")\n";
        return result;
    }

    @Override
    protected String prepareInit() {
        return "";
    }
    
}
